{-
 This file is part of the Clafer to Alloy Translator (clafer2alloy).

 Copyright (C) 2010 Kacper Bak <http://gsd.uwaterloo.ca/kbak>

 clafer2alloy is free software: you can redistribute it and/or modify
 it under the terms of the GNU Lesser General Public License as published by
 the Free Software Foundation, either version 3 of the License, or
 (at your option) any later version.

 clafer2alloy is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 GNU Lesser General Public License for more details.

 You should have received a copy of the GNU Lesser General Public License
 along with clafer2alloy. (See files COPYING and COPYING.LESSER.)  If not,
 see <http://www.gnu.org/licenses/>.
-}
module TypeEngine where

import Absclafer2alloy
import Common
import AlloyCode
import Monad
import Data.List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Graph
import Data.Tree
import Data.Array
import Data.Maybe
import Data.Function (on)
import Control.Monad.State

allGraphs n = map (buildG (1,n))
                  (subsequences [ (a,b) | a <- [1..n], b <- [1..n] ])

(g, vn, kv)  = graphFromEdges [("clafer", 0, []), ("a", 1, [0]), ("b", 2, [1])]

-- -----------------------------------------------------------------------------
-- environment carries predecessors
data TEnv = TEnv [Ident]

data ClaferType = Ref | Clafe | Abstract deriving Show
data Prop  = Prop ClaferType  deriving Show
type Symbol = ([Ident], Prop)
type SymbolTable = Map [Ident] (Prop, Ident)
data STEnv = STEnv {
  symt :: SymbolTable
}

isTopLevel (TEnv predecessors) = null predecessors

typeModule :: Module -> SymbolTable
typeModule x = case x of
  Module declarations -> symt $ execState (mapM typeDeclaration declarations) $
    STEnv Map.empty


typeDeclaration x = case x of
  EnumDecl ident enumids  -> error "typed"
  AbsClaferDecl gcard ident super attr elements  -> do
    typeItem env ident elements (Prop Abstract)
  ClaferDecl clafer  -> do typeClafer env clafer
  ConstDecl constraint  -> return ()
  where
  env = TEnv []


-- adds a symbol to the map
typeItem (TEnv predecessors) ident elements prop = do
  let predecessors' = ident : predecessors
  modify (\e -> e { symt = Map.insert predecessors'
    (prop, Ident $ symbolId ++ show (Map.size $ symt e)) (symt e) })
  typeElements (TEnv predecessors') elements


-- types non-abstract clafer
typeClafer env x = case x of
  Clafer gcard ident super attr essential card elements  -> do
    let clType = if isReference x && not (isTopLevel env) then Ref else Clafe
    typeItem env ident elements (Prop clType)
 

-- types subclafers
typeElements env x = case x of
  ElementsEmpty  -> error "desugred"
  Elements elements  -> do mapM_ (typeElement env) elements


-- types single subclafer
typeElement env x = case x of
  Subclafer clafer  -> do typeClafer env clafer
  ClaferUse name essential card elements -> error "desugared"
  Subconstraint constraint  -> return ()
